The present application relates generally to an improved data processing apparatus and method and more specifically to mechanisms for enhancing redundancy removal with early merging.
Many design automation algorithms have an objective of minimizing design size. For example, in logic synthesis, shrinking the design size is a way to save area and power on a die. In verification, shrinking the design size improves the scalability of the verification algorithms, because operating on a design of smaller size is often easier than operating on the original design. In addition, formal verification of safety properties involves finding a sequence of inputs such that a logical condition within the design is true or proving that no such sequence exists. While minimizing the size of a design, a discovery may be made that the logical condition may be replaced with a constant 0, implying that a condition may never be possible for the condition to be true and thus outright solving the formal verification problem.
One common way of minimizing the size of a design is by finding pairs of signals that are equivalent in every reachable state. If signals A and B are equivalent in every reachable state then they may be “merged,” an operation that replaces references to A with B and then removes A from the design or vice-versa. Induction is commonly used to prove that pairs of signals are equivalent on all reachable states. One form of induction, known as “k-induction,” involves two steps: in the “base case” a check is performed that all pairs of signals are equivalent under sequences of k states starting from any initial state. In the “inductive step,” a check is performed that, for every sequence of k+1 states that start from an arbitrary state, if all equivalences hold on the first k states in the sequence then the equivalences hold on the k+1′st state.
Prior work uses a k-induction formulation to prove that a set of equivalences hold in all reachable states. The work proves all equivalences simultaneously using a greatest fixed-point routine. Equivalences which do not pass the base case or inductive step checks are discarded and the algorithm tests the remaining equivalences anew. This process guarantees that the equivalences that remain once a fixed-point is reached will hold in all reachable states. The process may be scalably applied to large designs and widely used in nearly every logic synthesis and verification tool across the EDA industry.
However, the prior work suffers from one major problem: in that the prior work does not conclude that any equivalences are valid until a fixed-point is reached and, thus, the prior work cannot simplify the design until the fixed-point is reached. If computational resources are exceeded before the fixed-point is reached, then k-induction fails to find equivalences which can simplify the design.